#!/bin/bash
# Creates a benchmark output for the prover in CSV format to stdout,
# and also in HTML format into html/.
# @author Zoltan Kovacs <zoltan@geogebra.org>

# Setting defaults.
MY_VERSION=1.3

DEBUG=0 # In tmp/ there can be some log, if you set this to 1.
TIMEOUT=20
IMGHEIGHT=25
HTML=html/index.html
TEX=html/index.tex
PROVERS="Recio PureSymbolic Botana BotanaGiac OpenGeoProver_Wu OpenGeoProver_Area Auto Web"
TESTGGBURLBASE_GGBDIR=http://dev.geogebra.org/trac/browser/trunk/geogebra/test/scripts/benchmark/prover
GEOGEBRAWEB_URL1=https://www.geogebra.org/classic/?filename=https://dev.geogebra.org/trac/export
GEOGEBRAWEB_URL2=trunk/geogebra/test/scripts/benchmark/prover
SINGULARWSREMOTEURL=http://singularws.idm.jku.at/
USEENGINES=0
PROVEDETAILS=0 # Rewrite Prove[] to ProveDetails if set to 1

GEOGEBRADIR=../../../../
WEBCODEBASEDIR=$GEOGEBRADIR/web/war/web3d
ABSWEBDIR=`readlink -f $WEBCODEBASEDIR`

PHANTOMJS=`which phantomjs || echo unset`

usage() {
 echo "$0 - a benchmarking tool for GeoGebra's theorem prover subsystem"
 echo "Usage:"
 echo " xvfb-run $0 [options]"
 echo "  where options can be as follows (defaults in parentheses):"
 echo "   -S <name>    run scenario: 'name' can be one of the following: jar-paper, giac-test, ndg"
 echo "   -D           rewrite Prove commands to ProveDetails"
 echo "   -d           put some debugging logs into tmp/"
 echo "   -t <number>  timeout: exit from a single test after the given number of seconds ($TIMEOUT)"
 echo "   -H <number>  image height: show .ggb thumbnails in the given number of pixels ($IMGHEIGHT)"
 echo "   -o <file>    set name for output .html file ($HTML)"
 echo "   -T <file>    set name for output .tex file ($TEX)"
 echo "   -p <list>    space separated list of prover engines to test ($PROVERS)"
 echo "   -g <url>     use 'url' for putting links on test cases ($TESTGGBURLBASE_GGBDIR)"
 echo "   -s <url>     use 'url' to use non-default SingularWS ($SINGULARWSREMOTEURL)"
 echo "   -e           add introduction and use engine numbers in table headers"
 echo "   -r           run GeoGebra desktop version from the current sources"
 echo "   -P <path>    use path to run PhantomJS ($PHANTOMJS)"
 echo "   -h           show this help"
 echo "   -v           print script version"
 echo
 echo "Examples:"
 echo " xvfb-run $0 -S jar-paper -d    # creates an output like at http://ggb1.idm.jku.at/~kovzol/data/Prove-20141009/"
 echo " xvfb-run $0 -S giac-test -d    # compares Prove output for Botana and BotanaGiac"
 echo " xvfb-run $0 -S giac-test -D -d # compares ProveDetails output for Botana and BotanaGiac"
 echo " xvfb-run $0 -S ndg -d          # compares ProveDetails output for Botana, BotanaGiac and OpenGeoProver_Wu"
 echo " $0 -d -p Web -P \`pwd\`/phantomjs-2.0.0 # runs the Web test only (assuming PhantomJS is installed in '.')"
 echo "Note: You may want to use 'xvfb-run -a -s \"-screen 0 1024x768x24\" $0 ...' for 3D compatibility. Tested under Ubuntu 14.10."
 exit 0
 }

version() {
 echo "$0 version $MY_VERSION"
 exit 0
 }

while getopts "t:dH:o:T:p:P:S:eDhvr" OPT; do
 case $OPT in
  t)
   TIMEOUT="$OPTARG"
   ;;
  P)
   PHANTOMJS="$OPTARG"
   which $PHANTOMJS >/dev/null || {
    echo "FATAL: PhantomJS is not found in $PHANTOMJS (>= 2.0.0 needed)"
    exit 1
    }
   ;;
  d)
   DEBUG=1
   ;;
  H)
   IMGHEIGHT="$OPTARG"
   ;;
  o)
   HTML="$OPTARG"
   ;;
  T)
   TEX="$OPTARG"
   ;;
  p)
   PROVERS="$OPTARG"
   ;;
  S)
   case "$OPTARG" in
    jar-paper)
     PROVERS="Recio Botana BotanaGiac OpenGeoProver_Wu OpenGeoProver_Area Auto"
     USEENGINES=1
     ;;
    giac-test)
     PROVERS="Botana BotanaGiac"
     ;;
    ndg)
     PROVERS="Botana BotanaGiac OpenGeoProver_Wu Auto"
     PROVEDETAILS=1
     ;;
   esac # -S
   ;;
  e)
   USEENGINES=1
   ;;
  g)
   TESTGGBURLBASE_GGBDIR="$OPTARG"
   ;;
  s)
   SINGULARWSREMOTEURL="$OPTARG"
   ;;
  D)
   PROVEDETAILS=1
   ;;
  h)
   usage
   ;;
  v)
   version
   ;;
  r)
   RUNDIR=$GEOGEBRADIR/desktop/build/install/desktop/bin # run the "installDist" task in Gradle first
   BINBASE=./desktop
   # VERSION=`cd $RUNDIR; $BINBASE --v 2>&1 | head -1 | cut -f5 -d" "`

   ;;

 esac
done

# Put name of the filters into $@
shift $((OPTIND-1))

PROVERSNO=`echo $PROVERS | wc -w`
THISDIR=`dirname $0`
MYDIR=`cd $THISDIR; pwd`
mkdir -p $MYDIR/tmp $MYDIR/html
LOGFILE=$MYDIR/tmp/.test.log
REGRESSIONFILE=$MYDIR/tmp/.regression.out
JSFILE=$MYDIR/tmp/settings.js # this is hardcoded in jstest.html
rm -f $HTML $TEX

# Testing prerequisites:
prereq () {
 which $1 2>&1 >/dev/null || {
  echo "FATAL: No '$1' executable found. $2"
  exit 1
  }
 }

if [ "$RUNDIR" = "" ]; then
 prereq geogebra "Try installing GeoGebra first."
 BIN=`which geogebra`
 RUNDIR=`dirname $BIN`
 BINBASE="geogebra --2"
 fi
prereq unzip
prereq zip
prereq timeout

REVISION=`svn info | grep ^Revision: | cut -f2 -d" "`
if [ "$REVISION" != "" ]; then
 REVISION=" (r$REVISION)"
 fi
# public static final String VERSION_STRING = "5.0.122.0";
VERSION=`cat $GEOGEBRADIR/common/src/main/java/org/geogebra/common/GeoGebraConstants.java |\
grep " VERSION_STRING =" | awk '{print $7}' | sed s/\"//g | sed s/";"//`

# Title
TITLE="Prover benchmark for GeoGebra $VERSION$REVISION"
DATE=`date "+%Y-%m-%d %H:%M"`
HOST=`hostname`
echo "<!DOCTYPE html><html><head>
<title>$TITLE</title>
</head><body><h1>$TITLE</h1>
<h2>on $DATE at $HOST</h2><pre>" >> $HTML
HWINFO=`which hwinfo 2>&1 >/dev/null`
if [ "$HWINFO" = "" ]; then
 INFO=`lshw -quiet -class processor 2>/dev/null | grep product | cut -d: -f2`
else
 INFO=`hwinfo --short --cpu 2>&1 | grep CPU`
 fi
echo $INFO | sed 's/^[ \t]*//' >> $HTML
echo -n "</pre>" >> $HTML
echo "% http://tex.stackexchange.com/questions/50349/color-only-a-cell-of-a-table
\documentclass{article}
\usepackage[table]{xcolor}% http://ctan.org/pkg/xcolor
\usepackage{multirow}
\usepackage{longtable}
\usepackage{array}
\begin{document}
\scriptsize{" >> $TEX

# Header
echo -n "Test file;"
if [ "$USEENGINES" = 1 ]; then
 cat intro.html >> $MYDIR/$HTML
 fi
cat style.html >> $MYDIR/$HTML
echo "<table><tr><th rowspan=\"2\" colspan=\"2\">Test file</th>" >> $MYDIR/$HTML
RESULTCOLUMN=c
if [ $PROVEDETAILS = 1 ]; then
 RESULTCOLUMN="m{1cm}"
 fi
echo "\begin{longtable}{|l|*{$PROVERSNO}{${RESULTCOLUMN}r|}}
\hline
{\multirow{2}{*}{\bf Test}}" >> $MYDIR/$TEX
echo 
for j in $PROVERS; do
 if [ "$USEENGINES" = 1 ]; then
  case $j in
   Recio)
    TOPRINT="Engine 1"
    ;;
   Botana)
    TOPRINT="Engine 2"
    ;;
   BotanaGiac)
    TOPRINT="Engine 2, Giac"
    ;;
   OpenGeoProver_Wu)
    TOPRINT="Engine 3a"
    ;;
   OpenGeoProver_Area)
    TOPRINT="Engine 3b"
    ;;
   *)
    TOPRINT="$j"
    ;;
   esac
else
 TOPRINT=`echo $j | sed s/"_"/" "/`
  fi
 echo -n "$TOPRINT result;Speed;"
 echo "<th colspan=\"2\">$TOPRINT</th>" >> $MYDIR/$HTML
 echo "& \multicolumn{2}{c|}{\bf $TOPRINT}" | sed s/OpenGeoProver/OGP/g |\
  sed s/BotanaGiac/Giac/ | sed s/Botana/Singular/ >> $MYDIR/$TEX
 done
echo "</tr><tr>" >> $MYDIR/$HTML
echo "\\\\" >> $MYDIR/$TEX

for j in $PROVERS; do
 echo "<th>Result</th><th>Speed</th>" >> $MYDIR/$HTML
 echo "&R.&S." >> $MYDIR/$TEX
 rm -f $MYDIR/tmp/rinput-$j
 done

echo "</tr>" >> $MYDIR/$HTML
echo "\\\\ \hline" >> $MYDIR/$TEX
echo

# Content
TESTS=0
for i in `find -name '*.ggb' | sort`; do
 TESTS=`expr $TESTS + 1`
 # Creating thumbnail:
 cd $MYDIR
 DIRNAME=`dirname $i | sed s/"^\.\/tests\/"/""/`
 TEST=`basename $i`
 unzip $i geogebra_thumbnail.png >/dev/null 2>&1
 mv geogebra_thumbnail.png html/$TEST.png
 echo -n "$TEST;"
 # TODO: change "latest" to current revision:
 echo "<tr><td class=\"ex\"><a href=\"$TESTGGBURLBASE_GGBDIR/$i\">$TEST</a></td><td class=\"eximg\"><a href=\"${GEOGEBRAWEB_URL1}/latest/${GEOGEBRAWEB_URL2}/$i#\"><img src=\"$TEST.png\" style=\"height:${IMGHEIGHT}px;width:auto;\"></a></td>" >> $MYDIR/$HTML
 TEST=`echo $TEST | sed s/".ggb"//`
 if [ `expr ${#TEST} '>' 15` = 1 ]; then
  TEST=${TEST:0:10}\$\\ldots\$${TEST:(-2)}
  fi
 echo "\cellcolor{blue!10}$TEST " | sed s/".ggb"// >> $MYDIR/$TEX

 declare -A RESULTDATA
 declare -A RESULTCLASSDATA
 declare -A CELLCOLORDATA
 declare -A TIMEDATA
 BESTTIME=""
 WORSTTIME=""
 BESTPROVER=""
 WORSTPROVER=""

 if [ "$PROVEDETAILS" = 1 ]; then
  TMPDIR=tempdir
  mkdir -p $TMPDIR
  unzip $i -d $TMPDIR >/dev/null 2>&1
  sed -i s/Prove/ProveDetails/ $TMPDIR/geogebra.xml
  i=$i-ProveDetails
  rm -f $i
  zip -j -r $i $TMPDIR >/dev/null 2>&1
  rm -fR $TMPDIR
  fi

 for j in $PROVERS; do
  cd $MYDIR; cd $RUNDIR
  ENGINE=`echo $j | cut -f1 -d_`
  METHOD=""
  if [ $ENGINE = OpenGeoProver ]; then
   METHOD=`echo $j | cut -f2 -d_`
   fi
  unset SWSOPTS
  unset EXTRAOPTS
  if [ $ENGINE = BotanaGiac ]; then
   ENGINE=Botana
   SWSOPTS=",enable:false"
   EXTRAOPTS=--giac
  elif [ $ENGINE = Botana ]; then
   SWSOPTS=",enable:true,caching:false"
   fi

  # Testing:
  if [ "$ENGINE" = "Web" ]; then
   which $PHANTOMJS >/dev/null || {
    echo "FATAL: PhantomJS is not found in $PHANTOMJS (>= 2.0.0 needed)"
    exit 1
    }
   test -d $ABSWEBDIR || {
    echo; echo "FATAL: folder $ABSWEBDIR does not exist. You have to compile web platform first."
    exit 1
    }
   echo -n "var ggbBase64File = \"" > $JSFILE
   cat $MYDIR/$i | base64 -w0 >> $JSFILE
   echo "\";" >> $JSFILE
   echo "var html5codeBase = 'file://$ABSWEBDIR';" >> $JSFILE
   timeout $((TIMEOUT+2)) $PHANTOMJS $MYDIR/testurl.js "file:///$MYDIR/jstest.html" $TIMEOUT > $MYDIR/tmp/.test.stdout 2>$MYDIR/tmp/.test.stderr
   RETVAL=$?
   # 14:50:36.344 DEBUG: ?: Benchmarking: 1120 ms
   # 14:50:36.345 DEBUG: ?: OUTPUT for Prove: proof = true
   # 14:50:36.346 DEBUG: ?: all CAS up
   cat $MYDIR/tmp/.test.stdout | grep Benchmarking > $LOGFILE
   grep --silent "OUTPUT for Prove:" $MYDIR/tmp/.test.stdout && \
    tac $MYDIR/tmp/.test.stdout | grep "OUTPUT for Prove:" | head -1 | sed 's/\(.*\) = \(.*\)/OUTPUT for Prove or ProveDetails == null = \2/' > $REGRESSIONFILE
   grep --silent "OUTPUT for ProveDetails:" $MYDIR/tmp/.test.stdout && \
    tac $MYDIR/tmp/.test.stdout | grep "OUTPUT for ProveDetails:" | head -1 | sed 's/\(.*\) = \(.*\)/\2/' |\
    sed s/{//g | sed s/}//g | sed s/", "/" "/g | awk '{printf "ProveDetails == null = %s", $0}' > $REGRESSIONFILE
   grep --silent "STATEMENT IS UNKNOWN" $MYDIR/tmp/.test.stdout && echo "Prove or ProveDetails == null = undefined" > $REGRESSIONFILE
   grep --silent ^SEVERE: $MYDIR/tmp/.test.stdout && echo "Prove or ProveDetails == null = undefined" > $REGRESSIONFILE
   # List k = ProveDetails[j] == null = true "AreCollinear[D,E,A]" "AreEqual[f,k_1]" "AreEqual[f,l]" "AreParallel[d,e]" "AreParallel[f,g]" "AreParallel[h,i]"
  else
   timeout $TIMEOUT $BINBASE \
    --prover=engine:$ENGINE,method:$METHOD,timeout:$TIMEOUT --singularws=remoteurl:${SINGULARWSREMOTEURL}${SWSOPTS} \
    --logFile=$LOGFILE \
    --regressionFile=$REGRESSIONFILE --language=en $EXTRAOPTS $MYDIR/$i \
    >$MYDIR/tmp/.test.stdout 2>$MYDIR/tmp/.test.stderr
   RETVAL=$?
   fi

  if [ $RETVAL = 124 ]; then
   RESULT=""
   TIME=timeout
  else
   RESULT=`cat $REGRESSIONFILE | grep Prove | sed s/" null ="//g | sed s/'"'//g | sed 's/\(.*\) == \(.*\)/\2/' | sed 's/\(.*\) = \(.*\)/\2/'`
   TIME=`cat $LOGFILE | grep Benchmarking | awk '{s=s+$5; print s}' | tail -1` # collecting all entries
   if [ $DEBUG = 1 ]; then
    cp $REGRESSIONFILE $REGRESSIONFILE-$TEST-$j
    cp $LOGFILE $LOGFILE-$TEST-$j
    cp $MYDIR/tmp/.test.stdout $MYDIR/tmp/.test.stdout-$TEST-$j
    cp $MYDIR/tmp/.test.stderr $MYDIR/tmp/.test.stderr-$TEST-$j
    fi
   fi # No timeout
  if [ "$TIME" = "" ]; then
   # Probably running the process was unsuccessful (maybe killed for another reason than 124).
   # In this case we assume "timeout" and clean $RESULT (which should have been cleaned up earlier, actually, FIXME):
   RESULT=""
   TIME=timeout
   fi
  echo -n "$RESULT;$TIME;"
  RESULTCLASS=" class=\"o6\""
  CELLCOLOR="green!10"
  DIRNAMELENGTH=${#DIRNAME}
  if [ "${RESULT:0:$DIRNAMELENGTH}" != "$DIRNAME" ]; then
   if [ "$RESULT" = "undefined" -o "$RESULT" = "" -o "$RESULT" = "?" ]; then
    RESULTCLASS=" class=\"undefined\""
    CELLCOLOR="yellow!25"
   else
    RESULTCLASS=" class=\"error\""
    CELLCOLOR="red!25"
    fi
  else
   echo "$TIME" >> $MYDIR/tmp/rinput-$j
   VARNAME=$`echo $j`
   VALUE=`eval echo $VARNAME`
   eval $j=`expr $VALUE + 1`
   if [ $TIME -lt 1000 ]; then
    RESULTCLASS=" class=\"o5\""
    CELLCOLOR="green!20"
    fi
   if [ $TIME -lt 300 ]; then
    RESULTCLASS=" class=\"o4\""
    CELLCOLOR="green!30"
    fi
   if [ $TIME -lt 150 ]; then
    RESULTCLASS=" class=\"o3\""
    CELLCOLOR="green!40"
    fi
   if [ $TIME -lt 50 ]; then
    RESULTCLASS=" class=\"o2\""
    CELLCOLOR="green!50"
    fi
   if [ $TIME -lt 20 ]; then
    RESULTCLASS=" class=\"o1\""
    CELLCOLOR="green!60"
    fi
   fi
  RESULTCLASSDATA[$j]=$RESULTCLASS
  CELLCOLORDATA[$j]="$CELLCOLOR"
  RESULTDATA[$j]=$RESULT
  TIMEDATA[$j]=$TIME

  # Storing best and worst results
  if [ "$TIME" != "" -a "$RESULT" = "$DIRNAME" -a $j != Auto ]; then
   # First time result
   if [ "$BESTTIME" = "" ]; then
    BESTTIME=$TIME
    BESTPROVER=$j
   else
    # At least second time result
    if [ $TIME -lt $BESTTIME ]; then
     BESTTIME=$TIME
     BESTPROVER=$j
    else
     if [ "$WORSTTIME" = "" ]; then
      # Exactly the second time result
      WORSTTIME=$TIME 
      WORSTPROVER=$j
     else
      if [ $WORSTTIME -lt $TIME ]; then
       # More than second time result with worst current time
       WORSTTIME=$TIME
       WORSTPROVER=$j
       fi # end of >2, worst current
      fi # end of >2, not worst current
     fi # end of >=2
    fi # end of >=1, not best time current
   fi # end of >=1 (all cases)
  # echo "<td$RESULTCLASS>$RESULT</td><td$RESULTCLASS>$TIME</td>" >> $MYDIR/$HTML
  done # All provers done for this tests

 for j in $PROVERS; do
  RESULTCLASS=${RESULTCLASSDATA[$j]}
  CELLCOLOR=${CELLCOLORDATA[$j]}
  RESULT=${RESULTDATA[$j]}
  if [ "$RESULT" = undefined -o "$RESULT" = "?" ]; then
   RESULT=""
   fi
  TIME=${TIMEDATA[$j]}
  SUMCLASS=""
  SUMCLASSTEX=""
  if [ "$WORSTPROVER" = "$j" ]; then
   SUMCLASS="worst"
   SUMCLASSTEX="\sl"
   fi
  if [ "$BESTPROVER" = "$j" ]; then
   SUMCLASS="best"
   SUMCLASSTEX="\bf"
   fi
  echo "<td$RESULTCLASS>$RESULT</td><td$RESULTCLASS><p class=\"$SUMCLASS\">$TIME</p></td>" >> $MYDIR/$HTML
  # TeX related changes
  TRUE=t
  if [ $PROVEDETAILS = 1 ]; then
   TRUE=""
   fi
  RESULT=`echo $RESULT | sed s/true/$TRUE/g | sed s/false/f/g`
  RESULT=`echo $RESULT | sed s/"AreEqual\[\([A-Za-z0-9_]\+\),\([A-Za-z0-9_]\+\)\]"/"\$\\1=\\2\$"/g |\
   sed s/"AreParallel\[\([A-Za-z0-9_]\+\),\([A-Za-z0-9_]\+\)\]"/"\$\\1\\\\\\\\parallel \\2\$"/g |\
   sed s/"ArePerpendicular\[\([A-Za-z0-9_]\+\),\([A-Za-z0-9_]\+\)\]"/"\$\\1\\\\perp \\2\$"/g |\
   sed s/"AreCollinear\[\([A-Za-z0-9_]\+\),\([A-Za-z0-9_]\+\),\([A-Za-z0-9_]\+\)\]"/"\$\\\\\\\\overline{\\1\\2\\3}\$"/g |\
   sed s/"\\\\$ \\\\$"/"\$\\\\\\\\hfill\\\\\\\\newline\$"/g |\
   sed s/"\.\.\."/"\$\\\\\\\\ldots\$"/g`
  if [ "$TIME" = timeout ]; then
   TIME="t/o"
   fi
  echo "& \cellcolor{$CELLCOLOR}$RESULT & \cellcolor{$CELLCOLOR}{$SUMCLASSTEX $TIME} " >> $MYDIR/$TEX
  done

 echo
 echo "</tr>" >> $MYDIR/$HTML
 echo "\\\\ \\hline" >> $MYDIR/$TEX
 done # All tests done

# Summary
echo -n "Summary;"
echo "<tr><td class=\"summary\" colspan=\"2\"><b>Summary (of $TESTS)</b></td>" >> $MYDIR/$HTML
echo "{\bf Total (of $TESTS)}" >> $MYDIR/$TEX
for j in $PROVERS; do
 VARNAME=$`echo $j`
 VALUE=`eval echo $VARNAME`
 echo -n "$VALUE;;"
 echo "<td class=\"summary\" colspan=\"2\"><b>$VALUE</b></td>" >> $MYDIR/$HTML
 echo "&\multicolumn{2}{c|}{\bf $VALUE}" >> $MYDIR/$TEX
 done
echo "</tr>" >> $MYDIR/$HTML
echo "\\\\ \\hline" >> $MYDIR/$TEX
echo

echo "</tr></table></body></html>" >> $MYDIR/$HTML
echo "\end{longtable}
}
\end{document}" >> $MYDIR/$TEX
